package srt.tool;

import java.io.IOException;
import java.util.ArrayList;
import java.util.List;

import srt.ast.BinaryExpr;
import srt.ast.Expr;
import srt.ast.IntLiteral;
import srt.ast.Program;
import srt.ast.WhileStmt;
import srt.ast.visitor.impl.PrinterVisitor;
import srt.exec.ProcessExec;
import srt.tool.exception.ProcessTimeoutException;

//Tool Implementation
public class SRToolImpl implements SRTool {
	private Program program; // c-like program
	private CLArgs clArgs; // arguments
	private boolean bounded = false, isCompFlag = false;

	public SRToolImpl(Program p, CLArgs clArgs) {
		this.program = p;
		this.clArgs = clArgs;
		if (isCompFlag = clArgs.mode.equals(CLArgs.COMP)) {
			// runs only in COMP mode
			clArgs.unsoundBmc = false; // making BMC sound
			this.bounded = makeBounded(); // trying to make all loops bounded
			if (bounded) {
				clArgs.mode = CLArgs.BMC; // if all loops are bounded then BMC
			} else {
				clArgs.mode = CLArgs.INVGEN; // else INVGEN
			}
		}
	}

	public SRToolResult go() throws IOException, InterruptedException {

		String programText = "";

		System.out.println("\n----------START----------\n" + "IN MODE: "
				+ clArgs.mode + "\n");

		if (clArgs.verbose) {
			programText = new PrinterVisitor().visit(program);
		}

		if (clArgs.verbose) {
			System.out.println("\n----------CAND GEN----------\n");
		}
		// Candidate loop invariant Generation only for INVGEN mode
		if (clArgs.mode.equals(CLArgs.INVGEN)) {
			program = (Program) new CandidatesGenVisitor().visit(program);
		}

		if (clArgs.verbose) {
			programText = new PrinterVisitor().visit(program);
			System.out.println("\n----------HOUDINI----------\n" + programText);
		}

		// Houdini, only for HOUDINI and INVGEN modes
		if (clArgs.mode.equals(CLArgs.HOUDINI)
				|| clArgs.mode.equals(CLArgs.INVGEN)) {
			program = (Program) new HoudiniVisitor().visit(program);
		}

		// BMC loop unwinder in BMC mode
		if (clArgs.mode.equals(CLArgs.BMC)) {
			System.out.println("BMC");
			program = (Program) new LoopUnwinderVisitor(clArgs.unsoundBmc,
					clArgs.unwindDepth).visit(program);
		} else {
			// use loop body abstraction otherwise
			System.out.println("VERIFIER");
			program = (Program) new LoopAbstractionVisitor().visit(program);
		}

		if (clArgs.verbose) {
			programText = new PrinterVisitor().visit(program);
			System.out.println("\n----------LOOP-----------\n" + programText);
		}

		// Predication
		program = (Program) new PredicationVisitor().visit(program);

		if (clArgs.verbose) {
			programText = new PrinterVisitor().visit(program);
			System.out.println("\n----------PREDICATION-----------\n"
					+ programText);
		}

		// Making SSA form
		program = (Program) new SSAVisitor().visit(program);

		// Output the program as text after being transformed (for
		// debugging).
		if (clArgs.verbose) {
			programText = new PrinterVisitor().visit(program);
			System.out.println("\n----------SSA FORM-----------\n"
					+ programText);

		}

		// Collect the constraint expressions and variable names.
		CollectConstraintsVisitor ccv = new CollectConstraintsVisitor();
		ccv.visit(program);

		// SMT querry preparation
		SMTLIBQueryBuilder builder = new SMTLIBQueryBuilder(ccv);
		builder.buildQuery();

		String smtQuery = builder.getQuery();

		// Output the query for debugging
		if (clArgs.verbose) {
			System.out.println(smtQuery);
		}

		// Submit query to SMT solver.
		// You can use other solvers.
		// E.g. The command for cvc4 is: "cvc4", "--lang", "smt2"
		ProcessExec process = new ProcessExec("z3", "-smt2", "-in");
		String queryResult = "";
		try {
			queryResult = process.execute(smtQuery, clArgs.timeout);
		} catch (ProcessTimeoutException e) {
			if (clArgs.verbose) {
				System.out.println("Timeout!");
			}
			return SRToolResult.UNKNOWN;
		}

		// output query result for debugging
		if (clArgs.verbose) {
			System.out.println(queryResult);
		}
		
		//correction check
		if (queryResult.startsWith("unsat")) {
			return SRToolResult.CORRECT;

		}

		if (queryResult.startsWith("sat")) {
			return SRToolResult.INCORRECT;
		}

		return SRToolResult.UNKNOWN;

	}

	//if all loops made bounded return true
	// else return false
	private boolean makeBounded() {
		CollectConstraintsVisitor ccv = new CollectConstraintsVisitor();
		ccv.visit(program);

		Expr expr;
		List<WhileStmt> whileStmts = new ArrayList<WhileStmt>();

		if (clArgs.verbose) {
		String programText = new PrinterVisitor().visit(program);
		System.out.println("\n----------START BOUNDING-----------\n"
				+ programText);
		}

		//Approximation of bound using loop condition. If not possible then return false
		int tmp = 0;
		for (WhileStmt whileStmt : ccv.whileNodes) {
			if (whileStmt.getBound() == null) {
				try {
					expr = (BinaryExpr) whileStmt.getCondition();
					if (((BinaryExpr) expr).getRhs().getClass()
							.equals(IntLiteral.class)) {
						System.out.println(((IntLiteral) ((BinaryExpr) expr)
								.getRhs()).getValue() + "");
						if ((tmp = ((IntLiteral) ((BinaryExpr) expr).getRhs())
								.getValue()) <= 100) {

							whileStmts.add(new WhileStmt(expr, new IntLiteral(
									tmp), whileStmt.getInvariantList(),
									whileStmt.getBody()));
						} else {
							return false;
						}
					} else if (((BinaryExpr) expr).getLhs().getClass()
							.equals(IntLiteral.class)) {
						System.out.println(((IntLiteral) ((BinaryExpr) expr)
								.getLhs()).getValue() + "");
						if ((tmp = ((IntLiteral) ((BinaryExpr) expr).getLhs())
								.getValue()) <= 100) {

							whileStmts.add(new WhileStmt(expr, new IntLiteral(
									tmp), whileStmt.getInvariantList(),
									whileStmt.getBody()));
						} else {
							return false;
						}
					} else {
						return false;
					}

				} catch (ClassCastException e) {
					return false;
				}
			} else {
				whileStmts.add(whileStmt);
			}
		}

		program = (Program) new ReplacementVisitor(whileStmts).visit(program);

		if (clArgs.verbose) {
		String programText = new PrinterVisitor().visit(program);
		System.out.println("\n----------AFTER BOUNDING-----------\n"
				+ programText);
		}

		return true;
	}
}
